H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 1.6560000000000001 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/FiniteMap.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ LR

mainModule FiniteMap

((eltsFM_GE :: FiniteMap Char a -> Char -> [a]) :: FiniteMap Char a -> Char -> [a])

module FiniteMap where

import qualified Maybe
import qualified Prelude

data FiniteMap b a = EmptyFM | Branch b a Int (FiniteMap b a) (FiniteMap b a)

instance (Eq a, Eq b) => Eq (FiniteMap b a) where

eltsFM_GE :: Ord a => FiniteMap a b -> a -> [b]

eltsFM_GE

fm fr

foldFM_GE (\key elt rest ->elt : rest) [] fr fm

foldFM_GE :: Ord c => (c -> a -> b -> b) -> b -> c -> FiniteMap c a -> b

foldFM_GE

k z fr EmptyFM

foldFM_GE

k z fr (Branch key elt _ fm_l fm_r)

key >= fr

foldFM_GE k (k key elt (foldFM_GE k z fr fm_r)) fr fm_l

otherwise

foldFM_GE k z fr fm_r

module Maybe where

import qualified FiniteMap
import qualified Prelude

Lambda Reductions:
The following Lambda expression

\keyeltrest→elt : rest

is transformed to

eltsFM_GE0 key elt rest = elt : rest

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

mainModule FiniteMap

((eltsFM_GE :: FiniteMap Char a -> Char -> [a]) :: FiniteMap Char a -> Char -> [a])

module FiniteMap where

import qualified Maybe
import qualified Prelude

data FiniteMap b a = EmptyFM | Branch b a Int (FiniteMap b a) (FiniteMap b a)

instance (Eq a, Eq b) => Eq (FiniteMap b a) where

eltsFM_GE :: Ord a => FiniteMap a b -> a -> [b]

eltsFM_GE

fm fr

foldFM_GE eltsFM_GE0 [] fr fm

eltsFM_GE0

key elt rest

elt : rest

foldFM_GE :: Ord b => (b -> c -> a -> a) -> a -> b -> FiniteMap b c -> a

foldFM_GE

k z fr EmptyFM

foldFM_GE

k z fr (Branch key elt _ fm_l fm_r)

key >= fr

foldFM_GE k (k key elt (foldFM_GE k z fr fm_r)) fr fm_l

otherwise

foldFM_GE k z fr fm_r

module Maybe where

import qualified FiniteMap
import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

mainModule FiniteMap

((eltsFM_GE :: FiniteMap Char a -> Char -> [a]) :: FiniteMap Char a -> Char -> [a])

module FiniteMap where

import qualified Maybe
import qualified Prelude

data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b)

instance (Eq a, Eq b) => Eq (FiniteMap b a) where

eltsFM_GE :: Ord b => FiniteMap b a -> b -> [a]

eltsFM_GE

fm fr

foldFM_GE eltsFM_GE0 [] fr fm

eltsFM_GE0

key elt rest

elt : rest

foldFM_GE :: Ord c => (c -> b -> a -> a) -> a -> c -> FiniteMap c b -> a

foldFM_GE

k z fr EmptyFM

foldFM_GE

k z fr (Branch key elt vw fm_l fm_r)

key >= fr

foldFM_GE k (k key elt (foldFM_GE k z fr fm_r)) fr fm_l

otherwise

foldFM_GE k z fr fm_r

module Maybe where

import qualified FiniteMap
import qualified Prelude

Cond Reductions:
The following Function with conditions

foldFM_GE k z fr EmptyFM = z

foldFM_GE k z fr (Branch key elt vw fm_l fm_r)

| key >= fr

= foldFM_GE k (k key elt (foldFM_GE k z fr fm_r)) fr fm_l

| otherwise

= foldFM_GE k z fr fm_r

is transformed to

foldFM_GE k z fr EmptyFM = foldFM_GE3 k z fr EmptyFM

foldFM_GE k z fr (Branch key elt vw fm_l fm_r) = foldFM_GE2 k z fr (Branch key elt vw fm_l fm_r)

foldFM_GE0 k z fr key elt vw fm_l fm_r True = foldFM_GE k z fr fm_r

foldFM_GE1 k z fr key elt vw fm_l fm_r True = foldFM_GE k (k key elt (foldFM_GE k z fr fm_r)) fr fm_l

foldFM_GE1 k z fr key elt vw fm_l fm_r False = foldFM_GE0 k z fr key elt vw fm_l fm_r otherwise

foldFM_GE2 k z fr (Branch key elt vw fm_l fm_r) = foldFM_GE1 k z fr key elt vw fm_l fm_r (key >= fr)

foldFM_GE3 k z fr EmptyFM = z

foldFM_GE3 wv ww wx wy = foldFM_GE2 wv ww wx wy

The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

mainModule FiniteMap

(eltsFM_GE :: FiniteMap Char a -> Char -> [a])

module FiniteMap where

import qualified Maybe
import qualified Prelude

data FiniteMap b a = EmptyFM | Branch b a Int (FiniteMap b a) (FiniteMap b a)

instance (Eq a, Eq b) => Eq (FiniteMap b a) where

eltsFM_GE :: Ord b => FiniteMap b a -> b -> [a]

eltsFM_GE

fm fr

foldFM_GE eltsFM_GE0 [] fr fm

eltsFM_GE0

key elt rest

elt : rest

foldFM_GE :: Ord a => (a -> c -> b -> b) -> b -> a -> FiniteMap a c -> b

foldFM_GE	k z fr EmptyFM	=	foldFM_GE3 k z fr EmptyFM
foldFM_GE	k z fr (Branch key elt vw fm_l fm_r)	=	foldFM_GE2 k z fr (Branch key elt vw fm_l fm_r)

foldFM_GE0

k z fr key elt vw fm_l fm_r True

foldFM_GE k z fr fm_r

foldFM_GE1	k z fr key elt vw fm_l fm_r True	=	foldFM_GE k (k key elt (foldFM_GE k z fr fm_r)) fr fm_l
foldFM_GE1	k z fr key elt vw fm_l fm_r False	=	foldFM_GE0 k z fr key elt vw fm_l fm_r otherwise

foldFM_GE2

k z fr (Branch key elt vw fm_l fm_r)

foldFM_GE1 k z fr key elt vw fm_l fm_r (key >= fr)

foldFM_GE3	k z fr EmptyFM	=	z
foldFM_GE3	wv ww wx wy	=	foldFM_GE2 wv ww wx wy

module Maybe where

import qualified FiniteMap
import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="eltsFM_GE",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="eltsFM_GE wz3",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="eltsFM_GE wz3 wz4",fontsize=16,color="black",shape="triangle"];4 -> 5[label="",style="solid", color="black", weight=3];
5[label="foldFM_GE eltsFM_GE0 [] wz4 wz3",fontsize=16,color="burlywood",shape="triangle"];1087[label="wz3/EmptyFM",fontsize=10,color="white",style="solid",shape="box"];5 -> 1087[label="",style="solid", color="burlywood", weight=9];
1087 -> 6[label="",style="solid", color="burlywood", weight=3];
1088[label="wz3/Branch wz30 wz31 wz32 wz33 wz34",fontsize=10,color="white",style="solid",shape="box"];5 -> 1088[label="",style="solid", color="burlywood", weight=9];
1088 -> 7[label="",style="solid", color="burlywood", weight=3];
6[label="foldFM_GE eltsFM_GE0 [] wz4 EmptyFM",fontsize=16,color="black",shape="box"];6 -> 8[label="",style="solid", color="black", weight=3];
7[label="foldFM_GE eltsFM_GE0 [] wz4 (Branch wz30 wz31 wz32 wz33 wz34)",fontsize=16,color="black",shape="box"];7 -> 9[label="",style="solid", color="black", weight=3];
8[label="foldFM_GE3 eltsFM_GE0 [] wz4 EmptyFM",fontsize=16,color="black",shape="box"];8 -> 10[label="",style="solid", color="black", weight=3];
9[label="foldFM_GE2 eltsFM_GE0 [] wz4 (Branch wz30 wz31 wz32 wz33 wz34)",fontsize=16,color="black",shape="box"];9 -> 11[label="",style="solid", color="black", weight=3];
10[label="[]",fontsize=16,color="green",shape="box"];11[label="foldFM_GE1 eltsFM_GE0 [] wz4 wz30 wz31 wz32 wz33 wz34 (wz30 >= wz4)",fontsize=16,color="black",shape="box"];11 -> 12[label="",style="solid", color="black", weight=3];
12[label="foldFM_GE1 eltsFM_GE0 [] wz4 wz30 wz31 wz32 wz33 wz34 (compare wz30 wz4 /= LT)",fontsize=16,color="black",shape="box"];12 -> 13[label="",style="solid", color="black", weight=3];
13[label="foldFM_GE1 eltsFM_GE0 [] wz4 wz30 wz31 wz32 wz33 wz34 (not (compare wz30 wz4 == LT))",fontsize=16,color="black",shape="box"];13 -> 14[label="",style="solid", color="black", weight=3];
14[label="foldFM_GE1 eltsFM_GE0 [] wz4 wz30 wz31 wz32 wz33 wz34 (not (primCmpChar wz30 wz4 == LT))",fontsize=16,color="burlywood",shape="box"];1089[label="wz30/Char wz300",fontsize=10,color="white",style="solid",shape="box"];14 -> 1089[label="",style="solid", color="burlywood", weight=9];
1089 -> 15[label="",style="solid", color="burlywood", weight=3];
15[label="foldFM_GE1 eltsFM_GE0 [] wz4 (Char wz300) wz31 wz32 wz33 wz34 (not (primCmpChar (Char wz300) wz4 == LT))",fontsize=16,color="burlywood",shape="box"];1090[label="wz4/Char wz40",fontsize=10,color="white",style="solid",shape="box"];15 -> 1090[label="",style="solid", color="burlywood", weight=9];
1090 -> 16[label="",style="solid", color="burlywood", weight=3];
16[label="foldFM_GE1 eltsFM_GE0 [] (Char wz40) (Char wz300) wz31 wz32 wz33 wz34 (not (primCmpChar (Char wz300) (Char wz40) == LT))",fontsize=16,color="black",shape="box"];16 -> 17[label="",style="solid", color="black", weight=3];
17[label="foldFM_GE1 eltsFM_GE0 [] (Char wz40) (Char wz300) wz31 wz32 wz33 wz34 (not (primCmpNat wz300 wz40 == LT))",fontsize=16,color="burlywood",shape="box"];1091[label="wz300/Succ wz3000",fontsize=10,color="white",style="solid",shape="box"];17 -> 1091[label="",style="solid", color="burlywood", weight=9];
1091 -> 18[label="",style="solid", color="burlywood", weight=3];
1092[label="wz300/Zero",fontsize=10,color="white",style="solid",shape="box"];17 -> 1092[label="",style="solid", color="burlywood", weight=9];
1092 -> 19[label="",style="solid", color="burlywood", weight=3];
18[label="foldFM_GE1 eltsFM_GE0 [] (Char wz40) (Char (Succ wz3000)) wz31 wz32 wz33 wz34 (not (primCmpNat (Succ wz3000) wz40 == LT))",fontsize=16,color="burlywood",shape="box"];1093[label="wz40/Succ wz400",fontsize=10,color="white",style="solid",shape="box"];18 -> 1093[label="",style="solid", color="burlywood", weight=9];
1093 -> 20[label="",style="solid", color="burlywood", weight=3];
1094[label="wz40/Zero",fontsize=10,color="white",style="solid",shape="box"];18 -> 1094[label="",style="solid", color="burlywood", weight=9];
1094 -> 21[label="",style="solid", color="burlywood", weight=3];
19[label="foldFM_GE1 eltsFM_GE0 [] (Char wz40) (Char Zero) wz31 wz32 wz33 wz34 (not (primCmpNat Zero wz40 == LT))",fontsize=16,color="burlywood",shape="box"];1095[label="wz40/Succ wz400",fontsize=10,color="white",style="solid",shape="box"];19 -> 1095[label="",style="solid", color="burlywood", weight=9];
1095 -> 22[label="",style="solid", color="burlywood", weight=3];
1096[label="wz40/Zero",fontsize=10,color="white",style="solid",shape="box"];19 -> 1096[label="",style="solid", color="burlywood", weight=9];
1096 -> 23[label="",style="solid", color="burlywood", weight=3];
20[label="foldFM_GE1 eltsFM_GE0 [] (Char (Succ wz400)) (Char (Succ wz3000)) wz31 wz32 wz33 wz34 (not (primCmpNat (Succ wz3000) (Succ wz400) == LT))",fontsize=16,color="black",shape="box"];20 -> 24[label="",style="solid", color="black", weight=3];
21[label="foldFM_GE1 eltsFM_GE0 [] (Char Zero) (Char (Succ wz3000)) wz31 wz32 wz33 wz34 (not (primCmpNat (Succ wz3000) Zero == LT))",fontsize=16,color="black",shape="box"];21 -> 25[label="",style="solid", color="black", weight=3];
22[label="foldFM_GE1 eltsFM_GE0 [] (Char (Succ wz400)) (Char Zero) wz31 wz32 wz33 wz34 (not (primCmpNat Zero (Succ wz400) == LT))",fontsize=16,color="black",shape="box"];22 -> 26[label="",style="solid", color="black", weight=3];
23[label="foldFM_GE1 eltsFM_GE0 [] (Char Zero) (Char Zero) wz31 wz32 wz33 wz34 (not (primCmpNat Zero Zero == LT))",fontsize=16,color="black",shape="box"];23 -> 27[label="",style="solid", color="black", weight=3];
24 -> 963[label="",style="dashed", color="red", weight=0];
24[label="foldFM_GE1 eltsFM_GE0 [] (Char (Succ wz400)) (Char (Succ wz3000)) wz31 wz32 wz33 wz34 (not (primCmpNat wz3000 wz400 == LT))",fontsize=16,color="magenta"];24 -> 964[label="",style="dashed", color="magenta", weight=3];
24 -> 965[label="",style="dashed", color="magenta", weight=3];
24 -> 966[label="",style="dashed", color="magenta", weight=3];
24 -> 967[label="",style="dashed", color="magenta", weight=3];
24 -> 968[label="",style="dashed", color="magenta", weight=3];
24 -> 969[label="",style="dashed", color="magenta", weight=3];
24 -> 970[label="",style="dashed", color="magenta", weight=3];
24 -> 971[label="",style="dashed", color="magenta", weight=3];
24 -> 972[label="",style="dashed", color="magenta", weight=3];
25[label="foldFM_GE1 eltsFM_GE0 [] (Char Zero) (Char (Succ wz3000)) wz31 wz32 wz33 wz34 (not (GT == LT))",fontsize=16,color="black",shape="box"];25 -> 30[label="",style="solid", color="black", weight=3];
26[label="foldFM_GE1 eltsFM_GE0 [] (Char (Succ wz400)) (Char Zero) wz31 wz32 wz33 wz34 (not (LT == LT))",fontsize=16,color="black",shape="box"];26 -> 31[label="",style="solid", color="black", weight=3];
27[label="foldFM_GE1 eltsFM_GE0 [] (Char Zero) (Char Zero) wz31 wz32 wz33 wz34 (not (EQ == LT))",fontsize=16,color="black",shape="box"];27 -> 32[label="",style="solid", color="black", weight=3];
964[label="wz400",fontsize=16,color="green",shape="box"];965[label="wz34",fontsize=16,color="green",shape="box"];966[label="wz3000",fontsize=16,color="green",shape="box"];967[label="wz3000",fontsize=16,color="green",shape="box"];968[label="wz33",fontsize=16,color="green",shape="box"];969[label="wz400",fontsize=16,color="green",shape="box"];970[label="wz31",fontsize=16,color="green",shape="box"];971[label="wz32",fontsize=16,color="green",shape="box"];972[label="[]",fontsize=16,color="green",shape="box"];963[label="foldFM_GE1 eltsFM_GE0 wz103 (Char (Succ wz104)) (Char (Succ wz105)) wz106 wz107 wz108 wz109 (not (primCmpNat wz110 wz111 == LT))",fontsize=16,color="burlywood",shape="triangle"];1098[label="wz110/Succ wz1100",fontsize=10,color="white",style="solid",shape="box"];963 -> 1098[label="",style="solid", color="burlywood", weight=9];
1098 -> 1054[label="",style="solid", color="burlywood", weight=3];
1099[label="wz110/Zero",fontsize=10,color="white",style="solid",shape="box"];963 -> 1099[label="",style="solid", color="burlywood", weight=9];
1099 -> 1055[label="",style="solid", color="burlywood", weight=3];
30[label="foldFM_GE1 eltsFM_GE0 [] (Char Zero) (Char (Succ wz3000)) wz31 wz32 wz33 wz34 (not False)",fontsize=16,color="black",shape="box"];30 -> 37[label="",style="solid", color="black", weight=3];
31[label="foldFM_GE1 eltsFM_GE0 [] (Char (Succ wz400)) (Char Zero) wz31 wz32 wz33 wz34 (not True)",fontsize=16,color="black",shape="box"];31 -> 38[label="",style="solid", color="black", weight=3];
32[label="foldFM_GE1 eltsFM_GE0 [] (Char Zero) (Char Zero) wz31 wz32 wz33 wz34 (not False)",fontsize=16,color="black",shape="box"];32 -> 39[label="",style="solid", color="black", weight=3];
1054[label="foldFM_GE1 eltsFM_GE0 wz103 (Char (Succ wz104)) (Char (Succ wz105)) wz106 wz107 wz108 wz109 (not (primCmpNat (Succ wz1100) wz111 == LT))",fontsize=16,color="burlywood",shape="box"];1100[label="wz111/Succ wz1110",fontsize=10,color="white",style="solid",shape="box"];1054 -> 1100[label="",style="solid", color="burlywood", weight=9];
1100 -> 1056[label="",style="solid", color="burlywood", weight=3];
1101[label="wz111/Zero",fontsize=10,color="white",style="solid",shape="box"];1054 -> 1101[label="",style="solid", color="burlywood", weight=9];
1101 -> 1057[label="",style="solid", color="burlywood", weight=3];
1055[label="foldFM_GE1 eltsFM_GE0 wz103 (Char (Succ wz104)) (Char (Succ wz105)) wz106 wz107 wz108 wz109 (not (primCmpNat Zero wz111 == LT))",fontsize=16,color="burlywood",shape="box"];1102[label="wz111/Succ wz1110",fontsize=10,color="white",style="solid",shape="box"];1055 -> 1102[label="",style="solid", color="burlywood", weight=9];
1102 -> 1058[label="",style="solid", color="burlywood", weight=3];
1103[label="wz111/Zero",fontsize=10,color="white",style="solid",shape="box"];1055 -> 1103[label="",style="solid", color="burlywood", weight=9];
1103 -> 1059[label="",style="solid", color="burlywood", weight=3];
37[label="foldFM_GE1 eltsFM_GE0 [] (Char Zero) (Char (Succ wz3000)) wz31 wz32 wz33 wz34 True",fontsize=16,color="black",shape="box"];37 -> 44[label="",style="solid", color="black", weight=3];
38[label="foldFM_GE1 eltsFM_GE0 [] (Char (Succ wz400)) (Char Zero) wz31 wz32 wz33 wz34 False",fontsize=16,color="black",shape="box"];38 -> 45[label="",style="solid", color="black", weight=3];
39[label="foldFM_GE1 eltsFM_GE0 [] (Char Zero) (Char Zero) wz31 wz32 wz33 wz34 True",fontsize=16,color="black",shape="box"];39 -> 46[label="",style="solid", color="black", weight=3];
1056[label="foldFM_GE1 eltsFM_GE0 wz103 (Char (Succ wz104)) (Char (Succ wz105)) wz106 wz107 wz108 wz109 (not (primCmpNat (Succ wz1100) (Succ wz1110) == LT))",fontsize=16,color="black",shape="box"];1056 -> 1060[label="",style="solid", color="black", weight=3];
1057[label="foldFM_GE1 eltsFM_GE0 wz103 (Char (Succ wz104)) (Char (Succ wz105)) wz106 wz107 wz108 wz109 (not (primCmpNat (Succ wz1100) Zero == LT))",fontsize=16,color="black",shape="box"];1057 -> 1061[label="",style="solid", color="black", weight=3];
1058[label="foldFM_GE1 eltsFM_GE0 wz103 (Char (Succ wz104)) (Char (Succ wz105)) wz106 wz107 wz108 wz109 (not (primCmpNat Zero (Succ wz1110) == LT))",fontsize=16,color="black",shape="box"];1058 -> 1062[label="",style="solid", color="black", weight=3];
1059[label="foldFM_GE1 eltsFM_GE0 wz103 (Char (Succ wz104)) (Char (Succ wz105)) wz106 wz107 wz108 wz109 (not (primCmpNat Zero Zero == LT))",fontsize=16,color="black",shape="box"];1059 -> 1063[label="",style="solid", color="black", weight=3];
44 -> 52[label="",style="dashed", color="red", weight=0];
44[label="foldFM_GE eltsFM_GE0 (eltsFM_GE0 (Char (Succ wz3000)) wz31 (foldFM_GE eltsFM_GE0 [] (Char Zero) wz34)) (Char Zero) wz33",fontsize=16,color="magenta"];44 -> 53[label="",style="dashed", color="magenta", weight=3];
45[label="foldFM_GE0 eltsFM_GE0 [] (Char (Succ wz400)) (Char Zero) wz31 wz32 wz33 wz34 otherwise",fontsize=16,color="black",shape="box"];45 -> 54[label="",style="solid", color="black", weight=3];
46 -> 55[label="",style="dashed", color="red", weight=0];
46[label="foldFM_GE eltsFM_GE0 (eltsFM_GE0 (Char Zero) wz31 (foldFM_GE eltsFM_GE0 [] (Char Zero) wz34)) (Char Zero) wz33",fontsize=16,color="magenta"];46 -> 56[label="",style="dashed", color="magenta", weight=3];
1060 -> 963[label="",style="dashed", color="red", weight=0];
1060[label="foldFM_GE1 eltsFM_GE0 wz103 (Char (Succ wz104)) (Char (Succ wz105)) wz106 wz107 wz108 wz109 (not (primCmpNat wz1100 wz1110 == LT))",fontsize=16,color="magenta"];1060 -> 1064[label="",style="dashed", color="magenta", weight=3];
1060 -> 1065[label="",style="dashed", color="magenta", weight=3];
1061[label="foldFM_GE1 eltsFM_GE0 wz103 (Char (Succ wz104)) (Char (Succ wz105)) wz106 wz107 wz108 wz109 (not (GT == LT))",fontsize=16,color="black",shape="box"];1061 -> 1066[label="",style="solid", color="black", weight=3];
1062[label="foldFM_GE1 eltsFM_GE0 wz103 (Char (Succ wz104)) (Char (Succ wz105)) wz106 wz107 wz108 wz109 (not (LT == LT))",fontsize=16,color="black",shape="box"];1062 -> 1067[label="",style="solid", color="black", weight=3];
1063[label="foldFM_GE1 eltsFM_GE0 wz103 (Char (Succ wz104)) (Char (Succ wz105)) wz106 wz107 wz108 wz109 (not (EQ == LT))",fontsize=16,color="black",shape="box"];1063 -> 1068[label="",style="solid", color="black", weight=3];
53 -> 5[label="",style="dashed", color="red", weight=0];
53[label="foldFM_GE eltsFM_GE0 [] (Char Zero) wz34",fontsize=16,color="magenta"];53 -> 64[label="",style="dashed", color="magenta", weight=3];
53 -> 65[label="",style="dashed", color="magenta", weight=3];
52[label="foldFM_GE eltsFM_GE0 (eltsFM_GE0 (Char (Succ wz3000)) wz31 wz5) (Char Zero) wz33",fontsize=16,color="burlywood",shape="triangle"];1108[label="wz33/EmptyFM",fontsize=10,color="white",style="solid",shape="box"];52 -> 1108[label="",style="solid", color="burlywood", weight=9];
1108 -> 66[label="",style="solid", color="burlywood", weight=3];
1109[label="wz33/Branch wz330 wz331 wz332 wz333 wz334",fontsize=10,color="white",style="solid",shape="box"];52 -> 1109[label="",style="solid", color="burlywood", weight=9];
1109 -> 67[label="",style="solid", color="burlywood", weight=3];
54[label="foldFM_GE0 eltsFM_GE0 [] (Char (Succ wz400)) (Char Zero) wz31 wz32 wz33 wz34 True",fontsize=16,color="black",shape="box"];54 -> 68[label="",style="solid", color="black", weight=3];
56 -> 5[label="",style="dashed", color="red", weight=0];
56[label="foldFM_GE eltsFM_GE0 [] (Char Zero) wz34",fontsize=16,color="magenta"];56 -> 69[label="",style="dashed", color="magenta", weight=3];
56 -> 70[label="",style="dashed", color="magenta", weight=3];
55[label="foldFM_GE eltsFM_GE0 (eltsFM_GE0 (Char Zero) wz31 wz6) (Char Zero) wz33",fontsize=16,color="burlywood",shape="triangle"];1111[label="wz33/EmptyFM",fontsize=10,color="white",style="solid",shape="box"];55 -> 1111[label="",style="solid", color="burlywood", weight=9];
1111 -> 71[label="",style="solid", color="burlywood", weight=3];
1112[label="wz33/Branch wz330 wz331 wz332 wz333 wz334",fontsize=10,color="white",style="solid",shape="box"];55 -> 1112[label="",style="solid", color="burlywood", weight=9];
1112 -> 72[label="",style="solid", color="burlywood", weight=3];
1064[label="wz1110",fontsize=16,color="green",shape="box"];1065[label="wz1100",fontsize=16,color="green",shape="box"];1066[label="foldFM_GE1 eltsFM_GE0 wz103 (Char (Succ wz104)) (Char (Succ wz105)) wz106 wz107 wz108 wz109 (not False)",fontsize=16,color="black",shape="triangle"];1066 -> 1069[label="",style="solid", color="black", weight=3];
1067[label="foldFM_GE1 eltsFM_GE0 wz103 (Char (Succ wz104)) (Char (Succ wz105)) wz106 wz107 wz108 wz109 (not True)",fontsize=16,color="black",shape="box"];1067 -> 1070[label="",style="solid", color="black", weight=3];
1068 -> 1066[label="",style="dashed", color="red", weight=0];
1068[label="foldFM_GE1 eltsFM_GE0 wz103 (Char (Succ wz104)) (Char (Succ wz105)) wz106 wz107 wz108 wz109 (not False)",fontsize=16,color="magenta"];64[label="wz34",fontsize=16,color="green",shape="box"];65[label="Char Zero",fontsize=16,color="green",shape="box"];66[label="foldFM_GE eltsFM_GE0 (eltsFM_GE0 (Char (Succ wz3000)) wz31 wz5) (Char Zero) EmptyFM",fontsize=16,color="black",shape="box"];66 -> 80[label="",style="solid", color="black", weight=3];
67[label="foldFM_GE eltsFM_GE0 (eltsFM_GE0 (Char (Succ wz3000)) wz31 wz5) (Char Zero) (Branch wz330 wz331 wz332 wz333 wz334)",fontsize=16,color="black",shape="box"];67 -> 81[label="",style="solid", color="black", weight=3];
68 -> 494[label="",style="dashed", color="red", weight=0];
68[label="foldFM_GE eltsFM_GE0 [] (Char (Succ wz400)) wz34",fontsize=16,color="magenta"];68 -> 495[label="",style="dashed", color="magenta", weight=3];
68 -> 496[label="",style="dashed", color="magenta", weight=3];
68 -> 497[label="",style="dashed", color="magenta", weight=3];
69[label="wz34",fontsize=16,color="green",shape="box"];70[label="Char Zero",fontsize=16,color="green",shape="box"];71[label="foldFM_GE eltsFM_GE0 (eltsFM_GE0 (Char Zero) wz31 wz6) (Char Zero) EmptyFM",fontsize=16,color="black",shape="box"];71 -> 84[label="",style="solid", color="black", weight=3];
72[label="foldFM_GE eltsFM_GE0 (eltsFM_GE0 (Char Zero) wz31 wz6) (Char Zero) (Branch wz330 wz331 wz332 wz333 wz334)",fontsize=16,color="black",shape="box"];72 -> 85[label="",style="solid", color="black", weight=3];
1069[label="foldFM_GE1 eltsFM_GE0 wz103 (Char (Succ wz104)) (Char (Succ wz105)) wz106 wz107 wz108 wz109 True",fontsize=16,color="black",shape="box"];1069 -> 1071[label="",style="solid", color="black", weight=3];
1070[label="foldFM_GE1 eltsFM_GE0 wz103 (Char (Succ wz104)) (Char (Succ wz105)) wz106 wz107 wz108 wz109 False",fontsize=16,color="black",shape="box"];1070 -> 1072[label="",style="solid", color="black", weight=3];
80[label="foldFM_GE3 eltsFM_GE0 (eltsFM_GE0 (Char (Succ wz3000)) wz31 wz5) (Char Zero) EmptyFM",fontsize=16,color="black",shape="box"];80 -> 96[label="",style="solid", color="black", weight=3];
81[label="foldFM_GE2 eltsFM_GE0 (eltsFM_GE0 (Char (Succ wz3000)) wz31 wz5) (Char Zero) (Branch wz330 wz331 wz332 wz333 wz334)",fontsize=16,color="black",shape="box"];81 -> 97[label="",style="solid", color="black", weight=3];
495[label="wz34",fontsize=16,color="green",shape="box"];496[label="wz400",fontsize=16,color="green",shape="box"];497[label="[]",fontsize=16,color="green",shape="box"];494[label="foldFM_GE eltsFM_GE0 wz61 (Char (Succ wz48)) wz52",fontsize=16,color="burlywood",shape="triangle"];1115[label="wz52/EmptyFM",fontsize=10,color="white",style="solid",shape="box"];494 -> 1115[label="",style="solid", color="burlywood", weight=9];
1115 -> 548[label="",style="solid", color="burlywood", weight=3];
1116[label="wz52/Branch wz520 wz521 wz522 wz523 wz524",fontsize=10,color="white",style="solid",shape="box"];494 -> 1116[label="",style="solid", color="burlywood", weight=9];
1116 -> 549[label="",style="solid", color="burlywood", weight=3];
84[label="foldFM_GE3 eltsFM_GE0 (eltsFM_GE0 (Char Zero) wz31 wz6) (Char Zero) EmptyFM",fontsize=16,color="black",shape="box"];84 -> 98[label="",style="solid", color="black", weight=3];
85[label="foldFM_GE2 eltsFM_GE0 (eltsFM_GE0 (Char Zero) wz31 wz6) (Char Zero) (Branch wz330 wz331 wz332 wz333 wz334)",fontsize=16,color="black",shape="box"];85 -> 99[label="",style="solid", color="black", weight=3];
1071 -> 494[label="",style="dashed", color="red", weight=0];
1071[label="foldFM_GE eltsFM_GE0 (eltsFM_GE0 (Char (Succ wz105)) wz106 (foldFM_GE eltsFM_GE0 wz103 (Char (Succ wz104)) wz109)) (Char (Succ wz104)) wz108",fontsize=16,color="magenta"];1071 -> 1073[label="",style="dashed", color="magenta", weight=3];
1071 -> 1074[label="",style="dashed", color="magenta", weight=3];
1071 -> 1075[label="",style="dashed", color="magenta", weight=3];
1072[label="foldFM_GE0 eltsFM_GE0 wz103 (Char (Succ wz104)) (Char (Succ wz105)) wz106 wz107 wz108 wz109 otherwise",fontsize=16,color="black",shape="box"];1072 -> 1076[label="",style="solid", color="black", weight=3];
96[label="eltsFM_GE0 (Char (Succ wz3000)) wz31 wz5",fontsize=16,color="black",shape="triangle"];96 -> 116[label="",style="solid", color="black", weight=3];
97 -> 117[label="",style="dashed", color="red", weight=0];
97[label="foldFM_GE1 eltsFM_GE0 (eltsFM_GE0 (Char (Succ wz3000)) wz31 wz5) (Char Zero) wz330 wz331 wz332 wz333 wz334 (wz330 >= Char Zero)",fontsize=16,color="magenta"];97 -> 118[label="",style="dashed", color="magenta", weight=3];
548[label="foldFM_GE eltsFM_GE0 wz61 (Char (Succ wz48)) EmptyFM",fontsize=16,color="black",shape="box"];548 -> 626[label="",style="solid", color="black", weight=3];
549[label="foldFM_GE eltsFM_GE0 wz61 (Char (Succ wz48)) (Branch wz520 wz521 wz522 wz523 wz524)",fontsize=16,color="black",shape="box"];549 -> 627[label="",style="solid", color="black", weight=3];
98[label="eltsFM_GE0 (Char Zero) wz31 wz6",fontsize=16,color="black",shape="triangle"];98 -> 120[label="",style="solid", color="black", weight=3];
99 -> 117[label="",style="dashed", color="red", weight=0];
99[label="foldFM_GE1 eltsFM_GE0 (eltsFM_GE0 (Char Zero) wz31 wz6) (Char Zero) wz330 wz331 wz332 wz333 wz334 (wz330 >= Char Zero)",fontsize=16,color="magenta"];99 -> 119[label="",style="dashed", color="magenta", weight=3];
1073[label="wz108",fontsize=16,color="green",shape="box"];1074[label="wz104",fontsize=16,color="green",shape="box"];1075 -> 96[label="",style="dashed", color="red", weight=0];
1075[label="eltsFM_GE0 (Char (Succ wz105)) wz106 (foldFM_GE eltsFM_GE0 wz103 (Char (Succ wz104)) wz109)",fontsize=16,color="magenta"];1075 -> 1077[label="",style="dashed", color="magenta", weight=3];
1075 -> 1078[label="",style="dashed", color="magenta", weight=3];
1075 -> 1079[label="",style="dashed", color="magenta", weight=3];
1076[label="foldFM_GE0 eltsFM_GE0 wz103 (Char (Succ wz104)) (Char (Succ wz105)) wz106 wz107 wz108 wz109 True",fontsize=16,color="black",shape="box"];1076 -> 1080[label="",style="solid", color="black", weight=3];
116[label="wz31 : wz5",fontsize=16,color="green",shape="box"];118 -> 96[label="",style="dashed", color="red", weight=0];
118[label="eltsFM_GE0 (Char (Succ wz3000)) wz31 wz5",fontsize=16,color="magenta"];117[label="foldFM_GE1 eltsFM_GE0 wz9 (Char Zero) wz330 wz331 wz332 wz333 wz334 (wz330 >= Char Zero)",fontsize=16,color="black",shape="triangle"];117 -> 134[label="",style="solid", color="black", weight=3];
626[label="foldFM_GE3 eltsFM_GE0 wz61 (Char (Succ wz48)) EmptyFM",fontsize=16,color="black",shape="box"];626 -> 648[label="",style="solid", color="black", weight=3];
627[label="foldFM_GE2 eltsFM_GE0 wz61 (Char (Succ wz48)) (Branch wz520 wz521 wz522 wz523 wz524)",fontsize=16,color="black",shape="box"];627 -> 649[label="",style="solid", color="black", weight=3];
120[label="wz31 : wz6",fontsize=16,color="green",shape="box"];119 -> 98[label="",style="dashed", color="red", weight=0];
119[label="eltsFM_GE0 (Char Zero) wz31 wz6",fontsize=16,color="magenta"];1077[label="wz105",fontsize=16,color="green",shape="box"];1078[label="wz106",fontsize=16,color="green",shape="box"];1079 -> 494[label="",style="dashed", color="red", weight=0];
1079[label="foldFM_GE eltsFM_GE0 wz103 (Char (Succ wz104)) wz109",fontsize=16,color="magenta"];1079 -> 1081[label="",style="dashed", color="magenta", weight=3];
1079 -> 1082[label="",style="dashed", color="magenta", weight=3];
1079 -> 1083[label="",style="dashed", color="magenta", weight=3];
1080 -> 494[label="",style="dashed", color="red", weight=0];
1080[label="foldFM_GE eltsFM_GE0 wz103 (Char (Succ wz104)) wz109",fontsize=16,color="magenta"];1080 -> 1084[label="",style="dashed", color="magenta", weight=3];
1080 -> 1085[label="",style="dashed", color="magenta", weight=3];
1080 -> 1086[label="",style="dashed", color="magenta", weight=3];
134[label="foldFM_GE1 eltsFM_GE0 wz9 (Char Zero) wz330 wz331 wz332 wz333 wz334 (compare wz330 (Char Zero) /= LT)",fontsize=16,color="black",shape="box"];134 -> 150[label="",style="solid", color="black", weight=3];
648[label="wz61",fontsize=16,color="green",shape="box"];649[label="foldFM_GE1 eltsFM_GE0 wz61 (Char (Succ wz48)) wz520 wz521 wz522 wz523 wz524 (wz520 >= Char (Succ wz48))",fontsize=16,color="black",shape="box"];649 -> 657[label="",style="solid", color="black", weight=3];
1081[label="wz109",fontsize=16,color="green",shape="box"];1082[label="wz104",fontsize=16,color="green",shape="box"];1083[label="wz103",fontsize=16,color="green",shape="box"];1084[label="wz109",fontsize=16,color="green",shape="box"];1085[label="wz104",fontsize=16,color="green",shape="box"];1086[label="wz103",fontsize=16,color="green",shape="box"];150[label="foldFM_GE1 eltsFM_GE0 wz9 (Char Zero) wz330 wz331 wz332 wz333 wz334 (not (compare wz330 (Char Zero) == LT))",fontsize=16,color="black",shape="box"];150 -> 175[label="",style="solid", color="black", weight=3];
657[label="foldFM_GE1 eltsFM_GE0 wz61 (Char (Succ wz48)) wz520 wz521 wz522 wz523 wz524 (compare wz520 (Char (Succ wz48)) /= LT)",fontsize=16,color="black",shape="box"];657 -> 741[label="",style="solid", color="black", weight=3];
175[label="foldFM_GE1 eltsFM_GE0 wz9 (Char Zero) wz330 wz331 wz332 wz333 wz334 (not (primCmpChar wz330 (Char Zero) == LT))",fontsize=16,color="burlywood",shape="box"];1125[label="wz330/Char wz3300",fontsize=10,color="white",style="solid",shape="box"];175 -> 1125[label="",style="solid", color="burlywood", weight=9];
1125 -> 192[label="",style="solid", color="burlywood", weight=3];
741[label="foldFM_GE1 eltsFM_GE0 wz61 (Char (Succ wz48)) wz520 wz521 wz522 wz523 wz524 (not (compare wz520 (Char (Succ wz48)) == LT))",fontsize=16,color="black",shape="box"];741 -> 746[label="",style="solid", color="black", weight=3];
192[label="foldFM_GE1 eltsFM_GE0 wz9 (Char Zero) (Char wz3300) wz331 wz332 wz333 wz334 (not (primCmpChar (Char wz3300) (Char Zero) == LT))",fontsize=16,color="black",shape="box"];192 -> 205[label="",style="solid", color="black", weight=3];
746[label="foldFM_GE1 eltsFM_GE0 wz61 (Char (Succ wz48)) wz520 wz521 wz522 wz523 wz524 (not (primCmpChar wz520 (Char (Succ wz48)) == LT))",fontsize=16,color="burlywood",shape="box"];1126[label="wz520/Char wz5200",fontsize=10,color="white",style="solid",shape="box"];746 -> 1126[label="",style="solid", color="burlywood", weight=9];
1126 -> 751[label="",style="solid", color="burlywood", weight=3];
205[label="foldFM_GE1 eltsFM_GE0 wz9 (Char Zero) (Char wz3300) wz331 wz332 wz333 wz334 (not (primCmpNat wz3300 Zero == LT))",fontsize=16,color="burlywood",shape="box"];1127[label="wz3300/Succ wz33000",fontsize=10,color="white",style="solid",shape="box"];205 -> 1127[label="",style="solid", color="burlywood", weight=9];
1127 -> 222[label="",style="solid", color="burlywood", weight=3];
1128[label="wz3300/Zero",fontsize=10,color="white",style="solid",shape="box"];205 -> 1128[label="",style="solid", color="burlywood", weight=9];
1128 -> 223[label="",style="solid", color="burlywood", weight=3];
751[label="foldFM_GE1 eltsFM_GE0 wz61 (Char (Succ wz48)) (Char wz5200) wz521 wz522 wz523 wz524 (not (primCmpChar (Char wz5200) (Char (Succ wz48)) == LT))",fontsize=16,color="black",shape="box"];751 -> 757[label="",style="solid", color="black", weight=3];
222[label="foldFM_GE1 eltsFM_GE0 wz9 (Char Zero) (Char (Succ wz33000)) wz331 wz332 wz333 wz334 (not (primCmpNat (Succ wz33000) Zero == LT))",fontsize=16,color="black",shape="box"];222 -> 241[label="",style="solid", color="black", weight=3];
223[label="foldFM_GE1 eltsFM_GE0 wz9 (Char Zero) (Char Zero) wz331 wz332 wz333 wz334 (not (primCmpNat Zero Zero == LT))",fontsize=16,color="black",shape="box"];223 -> 242[label="",style="solid", color="black", weight=3];
757[label="foldFM_GE1 eltsFM_GE0 wz61 (Char (Succ wz48)) (Char wz5200) wz521 wz522 wz523 wz524 (not (primCmpNat wz5200 (Succ wz48) == LT))",fontsize=16,color="burlywood",shape="box"];1129[label="wz5200/Succ wz52000",fontsize=10,color="white",style="solid",shape="box"];757 -> 1129[label="",style="solid", color="burlywood", weight=9];
1129 -> 760[label="",style="solid", color="burlywood", weight=3];
1130[label="wz5200/Zero",fontsize=10,color="white",style="solid",shape="box"];757 -> 1130[label="",style="solid", color="burlywood", weight=9];
1130 -> 761[label="",style="solid", color="burlywood", weight=3];
241[label="foldFM_GE1 eltsFM_GE0 wz9 (Char Zero) (Char (Succ wz33000)) wz331 wz332 wz333 wz334 (not (GT == LT))",fontsize=16,color="black",shape="box"];241 -> 272[label="",style="solid", color="black", weight=3];
242[label="foldFM_GE1 eltsFM_GE0 wz9 (Char Zero) (Char Zero) wz331 wz332 wz333 wz334 (not (EQ == LT))",fontsize=16,color="black",shape="box"];242 -> 273[label="",style="solid", color="black", weight=3];
760[label="foldFM_GE1 eltsFM_GE0 wz61 (Char (Succ wz48)) (Char (Succ wz52000)) wz521 wz522 wz523 wz524 (not (primCmpNat (Succ wz52000) (Succ wz48) == LT))",fontsize=16,color="black",shape="box"];760 -> 764[label="",style="solid", color="black", weight=3];
761[label="foldFM_GE1 eltsFM_GE0 wz61 (Char (Succ wz48)) (Char Zero) wz521 wz522 wz523 wz524 (not (primCmpNat Zero (Succ wz48) == LT))",fontsize=16,color="black",shape="box"];761 -> 765[label="",style="solid", color="black", weight=3];
272[label="foldFM_GE1 eltsFM_GE0 wz9 (Char Zero) (Char (Succ wz33000)) wz331 wz332 wz333 wz334 (not False)",fontsize=16,color="black",shape="box"];272 -> 326[label="",style="solid", color="black", weight=3];
273[label="foldFM_GE1 eltsFM_GE0 wz9 (Char Zero) (Char Zero) wz331 wz332 wz333 wz334 (not False)",fontsize=16,color="black",shape="box"];273 -> 327[label="",style="solid", color="black", weight=3];
764 -> 963[label="",style="dashed", color="red", weight=0];
764[label="foldFM_GE1 eltsFM_GE0 wz61 (Char (Succ wz48)) (Char (Succ wz52000)) wz521 wz522 wz523 wz524 (not (primCmpNat wz52000 wz48 == LT))",fontsize=16,color="magenta"];764 -> 991[label="",style="dashed", color="magenta", weight=3];
764 -> 992[label="",style="dashed", color="magenta", weight=3];
764 -> 993[label="",style="dashed", color="magenta", weight=3];
764 -> 994[label="",style="dashed", color="magenta", weight=3];
764 -> 995[label="",style="dashed", color="magenta", weight=3];
764 -> 996[label="",style="dashed", color="magenta", weight=3];
764 -> 997[label="",style="dashed", color="magenta", weight=3];
764 -> 998[label="",style="dashed", color="magenta", weight=3];
764 -> 999[label="",style="dashed", color="magenta", weight=3];
765[label="foldFM_GE1 eltsFM_GE0 wz61 (Char (Succ wz48)) (Char Zero) wz521 wz522 wz523 wz524 (not (LT == LT))",fontsize=16,color="black",shape="box"];765 -> 772[label="",style="solid", color="black", weight=3];
326[label="foldFM_GE1 eltsFM_GE0 wz9 (Char Zero) (Char (Succ wz33000)) wz331 wz332 wz333 wz334 True",fontsize=16,color="black",shape="box"];326 -> 345[label="",style="solid", color="black", weight=3];
327[label="foldFM_GE1 eltsFM_GE0 wz9 (Char Zero) (Char Zero) wz331 wz332 wz333 wz334 True",fontsize=16,color="black",shape="box"];327 -> 346[label="",style="solid", color="black", weight=3];
991[label="wz48",fontsize=16,color="green",shape="box"];992[label="wz524",fontsize=16,color="green",shape="box"];993[label="wz52000",fontsize=16,color="green",shape="box"];994[label="wz52000",fontsize=16,color="green",shape="box"];995[label="wz523",fontsize=16,color="green",shape="box"];996[label="wz48",fontsize=16,color="green",shape="box"];997[label="wz521",fontsize=16,color="green",shape="box"];998[label="wz522",fontsize=16,color="green",shape="box"];999[label="wz61",fontsize=16,color="green",shape="box"];772[label="foldFM_GE1 eltsFM_GE0 wz61 (Char (Succ wz48)) (Char Zero) wz521 wz522 wz523 wz524 (not True)",fontsize=16,color="black",shape="box"];772 -> 781[label="",style="solid", color="black", weight=3];
345 -> 52[label="",style="dashed", color="red", weight=0];
345[label="foldFM_GE eltsFM_GE0 (eltsFM_GE0 (Char (Succ wz33000)) wz331 (foldFM_GE eltsFM_GE0 wz9 (Char Zero) wz334)) (Char Zero) wz333",fontsize=16,color="magenta"];345 -> 366[label="",style="dashed", color="magenta", weight=3];
345 -> 367[label="",style="dashed", color="magenta", weight=3];
345 -> 368[label="",style="dashed", color="magenta", weight=3];
345 -> 369[label="",style="dashed", color="magenta", weight=3];
346 -> 55[label="",style="dashed", color="red", weight=0];
346[label="foldFM_GE eltsFM_GE0 (eltsFM_GE0 (Char Zero) wz331 (foldFM_GE eltsFM_GE0 wz9 (Char Zero) wz334)) (Char Zero) wz333",fontsize=16,color="magenta"];346 -> 370[label="",style="dashed", color="magenta", weight=3];
346 -> 371[label="",style="dashed", color="magenta", weight=3];
346 -> 372[label="",style="dashed", color="magenta", weight=3];
781[label="foldFM_GE1 eltsFM_GE0 wz61 (Char (Succ wz48)) (Char Zero) wz521 wz522 wz523 wz524 False",fontsize=16,color="black",shape="box"];781 -> 792[label="",style="solid", color="black", weight=3];
366[label="wz33000",fontsize=16,color="green",shape="box"];367[label="wz331",fontsize=16,color="green",shape="box"];368[label="wz333",fontsize=16,color="green",shape="box"];369[label="foldFM_GE eltsFM_GE0 wz9 (Char Zero) wz334",fontsize=16,color="burlywood",shape="triangle"];1134[label="wz334/EmptyFM",fontsize=10,color="white",style="solid",shape="box"];369 -> 1134[label="",style="solid", color="burlywood", weight=9];
1134 -> 438[label="",style="solid", color="burlywood", weight=3];
1135[label="wz334/Branch wz3340 wz3341 wz3342 wz3343 wz3344",fontsize=10,color="white",style="solid",shape="box"];369 -> 1135[label="",style="solid", color="burlywood", weight=9];
1135 -> 439[label="",style="solid", color="burlywood", weight=3];
370[label="wz331",fontsize=16,color="green",shape="box"];371[label="wz333",fontsize=16,color="green",shape="box"];372 -> 369[label="",style="dashed", color="red", weight=0];
372[label="foldFM_GE eltsFM_GE0 wz9 (Char Zero) wz334",fontsize=16,color="magenta"];792[label="foldFM_GE0 eltsFM_GE0 wz61 (Char (Succ wz48)) (Char Zero) wz521 wz522 wz523 wz524 otherwise",fontsize=16,color="black",shape="box"];792 -> 798[label="",style="solid", color="black", weight=3];
438[label="foldFM_GE eltsFM_GE0 wz9 (Char Zero) EmptyFM",fontsize=16,color="black",shape="box"];438 -> 479[label="",style="solid", color="black", weight=3];
439[label="foldFM_GE eltsFM_GE0 wz9 (Char Zero) (Branch wz3340 wz3341 wz3342 wz3343 wz3344)",fontsize=16,color="black",shape="box"];439 -> 480[label="",style="solid", color="black", weight=3];
798[label="foldFM_GE0 eltsFM_GE0 wz61 (Char (Succ wz48)) (Char Zero) wz521 wz522 wz523 wz524 True",fontsize=16,color="black",shape="box"];798 -> 806[label="",style="solid", color="black", weight=3];
479[label="foldFM_GE3 eltsFM_GE0 wz9 (Char Zero) EmptyFM",fontsize=16,color="black",shape="box"];479 -> 563[label="",style="solid", color="black", weight=3];
480[label="foldFM_GE2 eltsFM_GE0 wz9 (Char Zero) (Branch wz3340 wz3341 wz3342 wz3343 wz3344)",fontsize=16,color="black",shape="box"];480 -> 564[label="",style="solid", color="black", weight=3];
806 -> 494[label="",style="dashed", color="red", weight=0];
806[label="foldFM_GE eltsFM_GE0 wz61 (Char (Succ wz48)) wz524",fontsize=16,color="magenta"];806 -> 814[label="",style="dashed", color="magenta", weight=3];
563[label="wz9",fontsize=16,color="green",shape="box"];564 -> 117[label="",style="dashed", color="red", weight=0];
564[label="foldFM_GE1 eltsFM_GE0 wz9 (Char Zero) wz3340 wz3341 wz3342 wz3343 wz3344 (wz3340 >= Char Zero)",fontsize=16,color="magenta"];564 -> 630[label="",style="dashed", color="magenta", weight=3];
564 -> 631[label="",style="dashed", color="magenta", weight=3];
564 -> 632[label="",style="dashed", color="magenta", weight=3];
564 -> 633[label="",style="dashed", color="magenta", weight=3];
564 -> 634[label="",style="dashed", color="magenta", weight=3];
814[label="wz524",fontsize=16,color="green",shape="box"];630[label="wz3344",fontsize=16,color="green",shape="box"];631[label="wz3340",fontsize=16,color="green",shape="box"];632[label="wz3341",fontsize=16,color="green",shape="box"];633[label="wz3343",fontsize=16,color="green",shape="box"];634[label="wz3342",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_foldFM_GE3(wz9, Branch(wz3340, wz3341, wz3342, wz3343, wz3344), h) → new_foldFM_GE1(wz9, wz3340, wz3341, wz3342, wz3343, wz3344, h)
new_foldFM_GE1(wz9, Char(Zero), wz331, wz332, wz333, wz334, h) → new_foldFM_GE2(wz331, new_foldFM_GE0(wz9, wz334, h), wz333, h)
new_foldFM_GE1(wz9, Char(Zero), wz331, wz332, wz333, wz334, h) → new_foldFM_GE3(wz9, wz334, h)
new_foldFM_GE(wz3000, wz31, wz5, Branch(wz330, wz331, wz332, wz333, wz334), h) → new_foldFM_GE1(new_eltsFM_GE0(wz3000, wz31, wz5, h), wz330, wz331, wz332, wz333, wz334, h)
new_foldFM_GE1(wz9, Char(Succ(wz33000)), wz331, wz332, wz333, wz334, h) → new_foldFM_GE(wz33000, wz331, new_foldFM_GE0(wz9, wz334, h), wz333, h)
new_foldFM_GE2(wz31, wz6, Branch(wz330, wz331, wz332, wz333, wz334), h) → new_foldFM_GE1(new_eltsFM_GE00(wz31, wz6, h), wz330, wz331, wz332, wz333, wz334, h)
new_foldFM_GE1(wz9, Char(Succ(wz33000)), wz331, wz332, wz333, Branch(wz3340, wz3341, wz3342, wz3343, wz3344), h) → new_foldFM_GE1(wz9, wz3340, wz3341, wz3342, wz3343, wz3344, h)

The TRS R consists of the following rules:

new_foldFM_GE10(wz9, Char(Zero), wz331, wz332, wz333, wz334, h) → new_foldFM_GE5(wz331, new_foldFM_GE0(wz9, wz334, h), wz333, h)
new_foldFM_GE4(wz3000, wz31, wz5, EmptyFM, h) → new_eltsFM_GE0(wz3000, wz31, wz5, h)
new_eltsFM_GE00(wz31, wz6, h) → :(wz31, wz6)
new_foldFM_GE4(wz3000, wz31, wz5, Branch(wz330, wz331, wz332, wz333, wz334), h) → new_foldFM_GE10(new_eltsFM_GE0(wz3000, wz31, wz5, h), wz330, wz331, wz332, wz333, wz334, h)
new_foldFM_GE5(wz31, wz6, EmptyFM, h) → new_eltsFM_GE00(wz31, wz6, h)
new_foldFM_GE0(wz9, EmptyFM, h) → wz9
new_foldFM_GE10(wz9, Char(Succ(wz33000)), wz331, wz332, wz333, wz334, h) → new_foldFM_GE4(wz33000, wz331, new_foldFM_GE0(wz9, wz334, h), wz333, h)
new_foldFM_GE5(wz31, wz6, Branch(wz330, wz331, wz332, wz333, wz334), h) → new_foldFM_GE10(new_eltsFM_GE00(wz31, wz6, h), wz330, wz331, wz332, wz333, wz334, h)
new_eltsFM_GE0(wz3000, wz31, wz5, h) → :(wz31, wz5)
new_foldFM_GE0(wz9, Branch(wz3340, wz3341, wz3342, wz3343, wz3344), h) → new_foldFM_GE10(wz9, wz3340, wz3341, wz3342, wz3343, wz3344, h)

The set Q consists of the following terms:

new_foldFM_GE0(x0, EmptyFM, x1)
new_eltsFM_GE0(x0, x1, x2, x3)
new_foldFM_GE0(x0, Branch(x1, x2, x3, x4, x5), x6)
new_eltsFM_GE00(x0, x1, x2)
new_foldFM_GE4(x0, x1, x2, Branch(x3, x4, x5, x6, x7), x8)
new_foldFM_GE10(x0, Char(Zero), x1, x2, x3, x4, x5)
new_foldFM_GE5(x0, x1, EmptyFM, x2)
new_foldFM_GE4(x0, x1, x2, EmptyFM, x3)
new_foldFM_GE10(x0, Char(Succ(x1)), x2, x3, x4, x5, x6)
new_foldFM_GE5(x0, x1, Branch(x2, x3, x4, x5, x6), x7)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_foldFM_GE1(wz9, Char(Zero), wz331, wz332, wz333, wz334, h) → new_foldFM_GE3(wz9, wz334, h)
The graph contains the following edges 1 >= 1, 6 >= 2, 7 >= 3
new_foldFM_GE1(wz9, Char(Succ(wz33000)), wz331, wz332, wz333, wz334, h) → new_foldFM_GE(wz33000, wz331, new_foldFM_GE0(wz9, wz334, h), wz333, h)
The graph contains the following edges 2 > 1, 3 >= 2, 5 >= 4, 7 >= 5
new_foldFM_GE1(wz9, Char(Succ(wz33000)), wz331, wz332, wz333, Branch(wz3340, wz3341, wz3342, wz3343, wz3344), h) → new_foldFM_GE1(wz9, wz3340, wz3341, wz3342, wz3343, wz3344, h)
The graph contains the following edges 1 >= 1, 6 > 2, 6 > 3, 6 > 4, 6 > 5, 6 > 6, 7 >= 7
new_foldFM_GE1(wz9, Char(Zero), wz331, wz332, wz333, wz334, h) → new_foldFM_GE2(wz331, new_foldFM_GE0(wz9, wz334, h), wz333, h)
The graph contains the following edges 3 >= 1, 5 >= 3, 7 >= 4
new_foldFM_GE3(wz9, Branch(wz3340, wz3341, wz3342, wz3343, wz3344), h) → new_foldFM_GE1(wz9, wz3340, wz3341, wz3342, wz3343, wz3344, h)
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3, 2 > 4, 2 > 5, 2 > 6, 3 >= 7
new_foldFM_GE2(wz31, wz6, Branch(wz330, wz331, wz332, wz333, wz334), h) → new_foldFM_GE1(new_eltsFM_GE00(wz31, wz6, h), wz330, wz331, wz332, wz333, wz334, h)
The graph contains the following edges 3 > 2, 3 > 3, 3 > 4, 3 > 5, 3 > 6, 4 >= 7
new_foldFM_GE(wz3000, wz31, wz5, Branch(wz330, wz331, wz332, wz333, wz334), h) → new_foldFM_GE1(new_eltsFM_GE0(wz3000, wz31, wz5, h), wz330, wz331, wz332, wz333, wz334, h)
The graph contains the following edges 4 > 2, 4 > 3, 4 > 4, 4 > 5, 4 > 6, 5 >= 7

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_foldFM_GE12(wz103, wz104, wz105, wz106, wz107, wz108, wz109, h) → new_foldFM_GE6(new_eltsFM_GE0(wz105, wz106, new_foldFM_GE7(wz103, wz104, wz109, h), h), wz104, wz108, h)
new_foldFM_GE12(wz103, wz104, wz105, wz106, wz107, wz108, wz109, h) → new_foldFM_GE6(wz103, wz104, wz109, h)
new_foldFM_GE6(wz61, wz48, Branch(Char(Succ(wz52000)), wz521, wz522, wz523, wz524), ba) → new_foldFM_GE11(wz61, wz48, wz52000, wz521, wz522, wz523, wz524, wz52000, wz48, ba)
new_foldFM_GE11(wz103, wz104, wz105, wz106, wz107, wz108, wz109, Succ(wz1100), Succ(wz1110), h) → new_foldFM_GE11(wz103, wz104, wz105, wz106, wz107, wz108, wz109, wz1100, wz1110, h)
new_foldFM_GE11(wz103, wz104, wz105, wz106, wz107, wz108, wz109, Succ(wz1100), Zero, h) → new_foldFM_GE6(new_eltsFM_GE0(wz105, wz106, new_foldFM_GE7(wz103, wz104, wz109, h), h), wz104, wz108, h)
new_foldFM_GE11(wz103, wz104, wz105, wz106, wz107, wz108, wz109, Zero, Zero, h) → new_foldFM_GE12(wz103, wz104, wz105, wz106, wz107, wz108, wz109, h)
new_foldFM_GE11(wz103, wz104, wz105, wz106, wz107, wz108, wz109, Succ(wz1100), Zero, h) → new_foldFM_GE6(wz103, wz104, wz109, h)
new_foldFM_GE11(wz103, wz104, wz105, wz106, wz107, wz108, wz109, Zero, Succ(wz1110), h) → new_foldFM_GE6(wz103, wz104, wz109, h)
new_foldFM_GE6(wz61, wz48, Branch(Char(Zero), wz521, wz522, wz523, wz524), ba) → new_foldFM_GE6(wz61, wz48, wz524, ba)

The TRS R consists of the following rules:

new_foldFM_GE7(wz61, wz48, EmptyFM, ba) → wz61
new_foldFM_GE7(wz61, wz48, Branch(Char(Succ(wz52000)), wz521, wz522, wz523, wz524), ba) → new_foldFM_GE13(wz61, wz48, wz52000, wz521, wz522, wz523, wz524, wz52000, wz48, ba)
new_foldFM_GE7(wz61, wz48, Branch(Char(Zero), wz521, wz522, wz523, wz524), ba) → new_foldFM_GE7(wz61, wz48, wz524, ba)
new_foldFM_GE13(wz103, wz104, wz105, wz106, wz107, wz108, wz109, Succ(wz1100), Succ(wz1110), h) → new_foldFM_GE13(wz103, wz104, wz105, wz106, wz107, wz108, wz109, wz1100, wz1110, h)
new_foldFM_GE13(wz103, wz104, wz105, wz106, wz107, wz108, wz109, Zero, Zero, h) → new_foldFM_GE14(wz103, wz104, wz105, wz106, wz107, wz108, wz109, h)
new_foldFM_GE13(wz103, wz104, wz105, wz106, wz107, wz108, wz109, Zero, Succ(wz1110), h) → new_foldFM_GE7(wz103, wz104, wz109, h)
new_foldFM_GE14(wz103, wz104, wz105, wz106, wz107, wz108, wz109, h) → new_foldFM_GE7(new_eltsFM_GE0(wz105, wz106, new_foldFM_GE7(wz103, wz104, wz109, h), h), wz104, wz108, h)
new_eltsFM_GE0(wz3000, wz31, wz5, bb) → :(wz31, wz5)
new_foldFM_GE13(wz103, wz104, wz105, wz106, wz107, wz108, wz109, Succ(wz1100), Zero, h) → new_foldFM_GE14(wz103, wz104, wz105, wz106, wz107, wz108, wz109, h)

The set Q consists of the following terms:

new_foldFM_GE13(x0, x1, x2, x3, x4, x5, x6, Succ(x7), Succ(x8), x9)
new_foldFM_GE13(x0, x1, x2, x3, x4, x5, x6, Succ(x7), Zero, x8)
new_foldFM_GE7(x0, x1, Branch(Char(Succ(x2)), x3, x4, x5, x6), x7)
new_foldFM_GE7(x0, x1, EmptyFM, x2)
new_foldFM_GE13(x0, x1, x2, x3, x4, x5, x6, Zero, Succ(x7), x8)
new_eltsFM_GE0(x0, x1, x2, x3)
new_foldFM_GE13(x0, x1, x2, x3, x4, x5, x6, Zero, Zero, x7)
new_foldFM_GE7(x0, x1, Branch(Char(Zero), x2, x3, x4, x5), x6)
new_foldFM_GE14(x0, x1, x2, x3, x4, x5, x6, x7)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_foldFM_GE6(wz61, wz48, Branch(Char(Succ(wz52000)), wz521, wz522, wz523, wz524), ba) → new_foldFM_GE11(wz61, wz48, wz52000, wz521, wz522, wz523, wz524, wz52000, wz48, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 3 > 4, 3 > 5, 3 > 6, 3 > 7, 3 > 8, 2 >= 9, 4 >= 10
new_foldFM_GE11(wz103, wz104, wz105, wz106, wz107, wz108, wz109, Zero, Zero, h) → new_foldFM_GE12(wz103, wz104, wz105, wz106, wz107, wz108, wz109, h)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 >= 6, 7 >= 7, 10 >= 8
new_foldFM_GE11(wz103, wz104, wz105, wz106, wz107, wz108, wz109, Succ(wz1100), Succ(wz1110), h) → new_foldFM_GE11(wz103, wz104, wz105, wz106, wz107, wz108, wz109, wz1100, wz1110, h)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 >= 6, 7 >= 7, 8 > 8, 9 > 9, 10 >= 10
new_foldFM_GE6(wz61, wz48, Branch(Char(Zero), wz521, wz522, wz523, wz524), ba) → new_foldFM_GE6(wz61, wz48, wz524, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 >= 4
new_foldFM_GE11(wz103, wz104, wz105, wz106, wz107, wz108, wz109, Succ(wz1100), Zero, h) → new_foldFM_GE6(new_eltsFM_GE0(wz105, wz106, new_foldFM_GE7(wz103, wz104, wz109, h), h), wz104, wz108, h)
The graph contains the following edges 2 >= 2, 6 >= 3, 10 >= 4
new_foldFM_GE11(wz103, wz104, wz105, wz106, wz107, wz108, wz109, Zero, Succ(wz1110), h) → new_foldFM_GE6(wz103, wz104, wz109, h)
The graph contains the following edges 1 >= 1, 2 >= 2, 7 >= 3, 10 >= 4
new_foldFM_GE11(wz103, wz104, wz105, wz106, wz107, wz108, wz109, Succ(wz1100), Zero, h) → new_foldFM_GE6(wz103, wz104, wz109, h)
The graph contains the following edges 1 >= 1, 2 >= 2, 7 >= 3, 10 >= 4
new_foldFM_GE12(wz103, wz104, wz105, wz106, wz107, wz108, wz109, h) → new_foldFM_GE6(wz103, wz104, wz109, h)
The graph contains the following edges 1 >= 1, 2 >= 2, 7 >= 3, 8 >= 4
new_foldFM_GE12(wz103, wz104, wz105, wz106, wz107, wz108, wz109, h) → new_foldFM_GE6(new_eltsFM_GE0(wz105, wz106, new_foldFM_GE7(wz103, wz104, wz109, h), h), wz104, wz108, h)
The graph contains the following edges 2 >= 2, 6 >= 3, 8 >= 4

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_foldFM_GE8(Char(Zero), Branch(Char(Zero), wz31, wz32, wz33, wz34), h) → new_foldFM_GE8(Char(Zero), wz34, h)
new_foldFM_GE8(Char(Zero), Branch(Char(Succ(wz3000)), wz31, wz32, wz33, wz34), h) → new_foldFM_GE8(Char(Zero), wz34, h)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_foldFM_GE8(Char(Zero), Branch(Char(Zero), wz31, wz32, wz33, wz34), h) → new_foldFM_GE8(Char(Zero), wz34, h)
The graph contains the following edges 1 >= 1, 2 > 1, 2 > 2, 3 >= 3
new_foldFM_GE8(Char(Zero), Branch(Char(Succ(wz3000)), wz31, wz32, wz33, wz34), h) → new_foldFM_GE8(Char(Zero), wz34, h)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3

foldFM_GE	k z fr EmptyFM	= foldFM_GE3 k z fr EmptyFM
foldFM_GE	k z fr (Branch key elt vw fm_l fm_r)	= foldFM_GE2 k z fr (Branch key elt vw fm_l fm_r)

foldFM_GE1	k z fr key elt vw fm_l fm_r True	= foldFM_GE k (k key elt (foldFM_GE k z fr fm_r)) fr fm_l
foldFM_GE1	k z fr key elt vw fm_l fm_r False	= foldFM_GE0 k z fr key elt vw fm_l fm_r otherwise